$\forall$${\it ds}$:fpf(Id; $x$.Type). normal{-}ds\{i:l\}(${\it ds}$) $\in$ prop\{i:l\}